es:event_system{i:l}, l:IdLnk, tgs:(Id List), da:fpf(Knd; k.Type), ds:fpf(Id; x.Type),
f:isect(((e':es-E(es). 
f:isect((es-isrcv(es; e'))
f:isect( (es-lnk(es; e') = l)
f:isect( (es-tag(es; e')  tgs)
f:isect( subtype_rel(es-valtype(es; e'); fpf-cap(da; Kind-deq; es-kind(es; e'); void)))
f:isect( (x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top))));
f:isect(z.({e:es-E(es)| loc(e) = source(l)  Id} ((tg:Id
f:isect(z.({e:es-E(es)| loc(e) = source(l)  Id} ( fpf-cap(da; Kind-deq; rcv(l,tg); void
f:isect(z.({e:es-E(es)| loc(e) = source(l)  Id} ( fpf-cap()) List))).
with decls ds dasends on l from e include f(e) and only these for tags in tgs  prop{i:l} 

latex

Definitions

t  T, P  Q, x:A. B(x), es-tag(es; e), ||as||, es-index(es; e), es-E(es), b, IdLnk, s = t, Id, (x  l), x:A  B(x), P  Q, A c B, x:A. B(x), True, void, Type, es-kind(es; e), rcv(l,tg), <a, b>, Knd, Kind-deq, x.A(x), x. t(x), T, x:AB(x), f(a), x(s), fpf(A; a.B(a)), EqDecider(T), fpf-cap(f; eq; x; z), es-valtype(es; e), es-val(es; e), P  Q, P  Q, source(l), loc(e), False, A, event_system{i:l}, type List, isect(A; x.B(x)), alle-at(es; i; e.P(e)), let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , a < b, guard(T), sq_type(T), prop{i:l}, sqequal(s; t), destination(l), es-sender(es; e), {x:A| B(x)} , ge(i; j), es-sends(es; l; e), es-Msgl(es; l), #$n, int_seg(i; j), l[i], A  B, , es-lnk(es; e), es-isrcv(es; e), lelt(i; j; k), top, id-deq, es-vartype(es; i; x), with decls ds dasends on l from e include f(e) and only these for tags in tgs

Lemmas

event system wf, es-kind wf, es-vartype wf, id-deq wf, top wf, alle-at wf, es-E wf, assert wf, es-isrcv wf, es-lnk wf, l member wf, subtype rel self, select wf, non neg length, int seg wf, length wf1, es-Msgl wf, es-sends wf, rcv wf, es-index wf, es-loc wf, es-sender wf, lsrc wf, ldst wf, IdLnk wf, IdLnk sq, es-loc-pred, es-loc-sender, Id wf, es-val wf, subtype rel wf, es-valtype wf, fpf-cap wf, squash wf, true wf, deq wf, fpf wf, Knd wf, Kind-deq wf, es-rcv-kind, es-tag wf